$\forall$$A$:Realizer, $i$:Id. $\neg$R{-}has{-}loc($A$;$i$) $\Rightarrow$ R{-}da($A$;$i$) $=$  $\in$ $k$:Knd fp$\rightarrow$ Type